FDL - Nuprl Lemma : fpf-map_wf

Nuprl Lemma : fpf-map_wf

A, C:Type, B:(A

Type), x:a:A fp

B(a), f:(a:{a:A| (a

fpf-domain(x))}

B(a)

C).
fpf-map(a,v.f(a,v);x)

(C List)

Definitions t T, x:A. B(x), (x l), x(s1,s2), x(s), fpf-map(a,v.f(a;v);x), a:A fp B(a), t.1, x. t(x), fpf-domain(f)

Lemmas fpf wf, map-wf2, l member wf